ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x,T:top, ks:(top List), a:top, snd:msg-spec(ds; da), j:Id.
sqequal(R-has-loc(ecl-machine3(ds; da; x; T; ks; a; snd); j);
sqequal(if null(ks)
sqequal(then reduce((l,b. bor(band((null(ecl-tags(l; snd))); eq_id(source(l); j)); b));
sqequal(then reduce(ff;
sqequal(then reduce(remove-repeats(idlnk-deq; msg-spec-links(snd)))
sqequal(else reduce((l,b. bor(eq_id(source(l); j); b));
sqequal(else reduce(ff;
sqequal(else reduce(remove-repeats(idlnk-deq; msg-spec-links(snd)))
sqequal(fi ) 

latex

Definitions

, t  T, x:A. B(x), top, [], prop{i:l}, b, Type, A, b, x:AB(x), P  Q, x:A  B(x), P  Q, P  Q, Unit, left + right, void, isect(A; x.B(x)), Id, subtype(S; T), ecl-tags(l; snd), bor(p; q), <a, b>, guard(T), sq_type(T), sqequal(s; t), x. t(x), ecl-machine3(ds; da; x; T; ks; a; snd), fpf(A; a.B(a)), Knd, msg-spec(ds; da), null(as), msg-spec-links(snd), idlnk-deq, remove-repeats(eq; L), IdLnk, type List, s = t

Lemmas

msg-spec wf, Knd wf, fpf wf, remove-repeats wf, idlnk-deq wf, msg-spec-links wf, Rall-has-loc, IdLnk wf, bool sq, R-lnk-tags-loc, ecl-tags wf, Id wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of null, bnot wf, not wf, assert wf, top wf, null wf3, bool wf